
/** Type refinement: A desugarized formula does not contain an Imply node.
                       This condition must hold recursively over the whole tree
*/
/* constraint (\forall f. f \in DesugaredFormula <-->
                         ( f \in Tru |
                           f \in Flse |
                          (f \in Neg & Neg_getField_f(f) \in DesugaredFormula) |
                          (f \in IOr & IOr_getField_left(f) \in DesugaredFormula & IOr_getField_right(f) \in DesugaredFormula) |
                          (f \in IAnd & IAnd_getField_left(f) \in DesugaredFormula & IAnd_getField_right(f) \in DesugaredFormula)
                         )) 
*/
  
/* domain  
              Dom_IOr = IOr &
              Dom_IAnd = IAnd &
              Dom_Neg = Neg &
              Dom_Tru = Tru &
              Dom_Flse = Flse &
              Dom_IImply = IImply
*/

sealed abstract class IFormula
class IAnd(val left: IFormula, val right: IFormula) extends IFormula
class IOr(val left: IFormula, val right: IFormula) extends IFormula
class Neg(val f: IFormula) extends IFormula
class Tru extends IFormula
class Flse extends IFormula
class IImply(val left: IFormula, val right: IFormula) extends IFormula


object IAnd {
  def apply(left: IFormula, right: IFormula): IAnd = 
    /* postcondition (left \in DesugaredFormula & right \in DesugaredFormula) --> res \in DesugaredFormula
     */
    new IAnd(left,right)
    
  def unapply(f: IAnd): Option[(IFormula,IFormula)] =
    /* postcondition f \in DesugaredFormula --> (res1 \in DesugaredFormula & res2 \in DesugaredFormula) */
    Some(Tuple2(f.left,f.right))
}

object IOr {
  def apply(left: IFormula, right: IFormula): IOr =
    /* postcondition (left \in DesugaredFormula & right \in DesugaredFormula) --> res \in DesugaredFormula
     */
    new IOr(left,right)
    
    
  def unapply(f: IOr): Option[(IFormula,IFormula)] =
    /* postcondition f \in DesugaredFormula --> (res1 \in DesugaredFormula & res2 \in DesugaredFormula) */
    Some(Tuple2(f.left,f.right))
}

object Neg {
  def apply(f: IFormula): Neg =
    /* postcondition (f \in DesugaredFormula) --> res \in DesugaredFormula
     */
    new Neg(f)
    
    
  def unapply(f: Neg): Option[IFormula] =
    /* postcondition f \in DesugaredFormula --> res1 \in DesugaredFormula */
    Some(f.f)
}


object IImply {
  def apply(left: IFormula, right: IFormula): IImply =
    /* postcondition (left \in DesugaredFormula & right \in DesugaredFormula) --> ~(res \in DesugaredFormula)
     */
    new IImply(left,right)
    
    
  def unapply(i: IImply): Option[(IFormula,IFormula)] =
    Some(Tuple2(i.left,i.right))
}

object Tru {
  def apply(): Tru =
    /* postcondition res \in DesugaredFormula
     */
    new Tru()
  def unapply(t: Tru): Boolean = true
}

object Flse {
  def apply(): Flse =
    /* postcondition res \in DesugaredFormula
     */
    new Flse()
  def unapply(f: Flse): Boolean = true 
}


class Desugar {
  
  def apply(f: IFormula): IFormula = 
  /** postcondition res \in DesugaredFormula */
    (f : IFormula) match {
      case t: Tru                                  => t
      case f: Flse                                 => f
      case IAnd(left: IFormula, right: IFormula)   => IAnd(this.apply(left),this.apply(right))
      case IOr(left: IFormula, right: IFormula)    => IOr(this.apply(left),this.apply(right))
      case Neg(f: IFormula)                        => Neg(this.apply(f))
      case IImply(left: IFormula, right: IFormula) => IOr(Neg(this.apply(left)),this.apply(right))
    }
  
  
  /**
    This examples is interesting because uses method desugarize postcondition
    in order to prove completeness of the PM.
  */
  def isDesugared(f: IFormula): Boolean =
    /** EXHAUSTIVENESS FAILS since the postcondition of the 'apply' method
    is in comment. Hence, the IImply pattern is missing*/
  (this.apply(f) : IFormula) match {
    case IAnd(left: IFormula, right: IFormula)   => this.isDesugared(left) && this.isDesugared(right)
    case IOr(left: IFormula, right: IFormula)    => this.isDesugared(left) && this.isDesugared(right)
    case Neg(f: IFormula)                        => this.isDesugared(f)
    case t: Tru                                  => t
    case f: Flse                                 => f
  }
}

object Main {

  def main(args: Array[String]): Unit =
    new Desugar().apply(IImply(IImply(Tru(),Flse()),Flse()))
}
  